(set-logic BV)

(define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001))
(define-fun shr4 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000004))
(define-fun shr16 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000010))
(define-fun shl1 ((x (BitVec 64))) (BitVec 64) (bvshl x #x0000000000000001))
(define-fun if0 ((x (BitVec 64)) (y (BitVec 64)) (z (BitVec 64))) (BitVec 64) (ite (= x #x0000000000000001) y z))

(synth-fun f ( (x (BitVec 64))) (BitVec 64)
(

(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)
                    (shl1 Start)
 		    (shr1 Start)
		    (shr4 Start)
		    (shr16 Start)
		    (bvand Start Start)
		    (bvor Start Start)
		    (bvxor Start Start)
		    (bvadd Start Start)
		    (if0 Start Start Start)
 ))
)
)
(constraint (= (f #x5C117C84D8F40A81) #x0000000080802406))
(constraint (= (f #x408E6C903F8904A3) #x0000000000600080))
(constraint (= (f #x35AFB29B6958F8ED) #x000000012D14904A))
(constraint (= (f #x7EE40697DDCF238D) #x00000003202034AE))
(constraint (= (f #x47505BC5681443A1) #x0000000202820A00))
(constraint (= (f #xCEB11B58EBD49071) #x314EE4A7142B6F8F))
(constraint (= (f #x903CA9D148E524BF) #x6FC3562EB71ADB41))
(constraint (= (f #xEBD87B67A1F3381B) #x142784985E0CC7E5))
(constraint (= (f #x63C4C7C04D7848D7) #x9C3B383FB287B729))
(constraint (= (f #xB9C6C61BA8431FB5) #x463939E457BCE04B))
(constraint (= (f #x5BED4BFE2C383CF0) #xA412B401D3C7C30E))
(constraint (= (f #xCF9F45EE7790F736) #x3060BA11886F08C8))
(constraint (= (f #x0C60E2AD703091B2) #xF39F1D528FCF6E4C))
(constraint (= (f #x7A1CE5D0087DAA18) #x85E31A2FF78255E6))
(constraint (= (f #xE241EA95F5644914) #x1DBE156A0A9BB6EA))
(constraint (= (f #xF0F0F0F0F0F0F0F1) #xFFFFFFFFFFFFFFFF))
(constraint (= (f #xC956DCEED008D5C8) #x36A923112FF72A36))
(constraint (= (f #xED7CF00F1BD11A40) #x12830FF0E42EE5BE))
(constraint (= (f #x5280EEC76CAC6924) #xAD7F1138935396DA))
(constraint (= (f #x1A5F336A0DF31F6E) #xE5A0CC95F20CE090))
(constraint (= (f #xF5BC736DFF5FE28A) #x0A438C9200A01D74))
(constraint (= (f #x0000000000000000) #xFFFFFFFFFFFFFFFE))
(check-synth)
